In computer science, a loop is a programming language statement which allows code to be repeatedly executed; an invariant of a loop is a property that holds before (and after) each repetition. It is a logical assertion, sometimes programmed as an assertion. Knowing its invariant(s) is essential for understanding the effect of a loop. In formal pro...